H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 22.128 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ IFR

mainModule List

((union :: [Int] -> [Int] -> [Int]) :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	_ _ []	=	[]
deleteBy	eq x (y : ys)	=	if x `eq` y then ys else y : deleteBy eq x ys

elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool

elem_by	_ _ []	=	False
elem_by	eq y (x : xs)	=	x `eq` y \|\| elem_by eq y xs

nubBy :: (a -> a -> Bool) -> [a] -> [a]

nubBy

eq l

nubBy' l []

where

nubBy'

[] _

[]

nubBy'

(y : ys) xs

elem_by eq y xs

nubBy' ys xs

otherwise

y : nubBy' ys (y : xs)

union :: Eq a => [a] -> [a] -> [a]

union

unionBy (==)

unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

unionBy

eq xs ys

xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

module Maybe where

import qualified List
import qualified Prelude

If Reductions:
The following If expression

if eq x y then ys else y : deleteBy eq x ys

is transformed to

deleteBy0 ys y eq x True = ys

deleteBy0 ys y eq x False = y : deleteBy eq x ys

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

mainModule List

((union :: [Int] -> [Int] -> [Int]) :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	_ _ []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool

elem_by	_ _ []	=	False
elem_by	eq y (x : xs)	=	x `eq` y \|\| elem_by eq y xs

nubBy :: (a -> a -> Bool) -> [a] -> [a]

nubBy

eq l

nubBy' l []

where

nubBy'

[] _

[]

nubBy'

(y : ys) xs

elem_by eq y xs

nubBy' ys xs

otherwise

y : nubBy' ys (y : xs)

union :: Eq a => [a] -> [a] -> [a]

union

unionBy (==)

unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

unionBy

eq xs ys

xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((union :: [Int] -> [Int] -> [Int]) :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	vw vx []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool

elem_by	vz wu []	=	False
elem_by	eq y (x : xs)	=	x `eq` y \|\| elem_by eq y xs

nubBy :: (a -> a -> Bool) -> [a] -> [a]

nubBy

eq l

nubBy' l []

where

nubBy'

[] vy

[]

nubBy'

(y : ys) xs

elem_by eq y xs

nubBy' ys xs

otherwise

y : nubBy' ys (y : xs)

union :: Eq a => [a] -> [a] -> [a]

union

unionBy (==)

unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

unionBy

eq xs ys

xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

nubBy' [] vy = []

nubBy' (y : ys) xs

| elem_by eq y xs

= nubBy' ys xs

| otherwise

= y : nubBy' ys (y : xs)

is transformed to

nubBy' [] vy = nubBy'3 [] vy

nubBy' (y : ys) xs = nubBy'2 (y : ys) xs

nubBy'1 y ys xs True = nubBy' ys xs

nubBy'1 y ys xs False = nubBy'0 y ys xs otherwise

nubBy'0 y ys xs True = y : nubBy' ys (y : xs)

nubBy'2 (y : ys) xs = nubBy'1 y ys xs (elem_by eq y xs)

nubBy'3 [] vy = []

nubBy'3 xv xw = nubBy'2 xv xw

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule List

((union :: [Int] -> [Int] -> [Int]) :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	vw vx []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool

elem_by	vz wu []	=	False
elem_by	eq y (x : xs)	=	x `eq` y \|\| elem_by eq y xs

nubBy :: (a -> a -> Bool) -> [a] -> [a]

nubBy

eq l

nubBy' l []

where

nubBy'	[] vy	=	nubBy'3 [] vy
nubBy'	(y : ys) xs	=	nubBy'2 (y : ys) xs

nubBy'0

y ys xs True

y : nubBy' ys (y : xs)

nubBy'1	y ys xs True	=	nubBy' ys xs
nubBy'1	y ys xs False	=	nubBy'0 y ys xs otherwise

nubBy'2

(y : ys) xs

nubBy'1 y ys xs (elem_by eq y xs)

nubBy'3	[] vy	=	[]
nubBy'3	xv xw	=	nubBy'2 xv xw

union :: Eq a => [a] -> [a] -> [a]

union

unionBy (==)

unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

unionBy

eq xs ys

xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

module Maybe where

import qualified List
import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

nubBy' l []

where

nubBy' [] vy = nubBy'3 [] vy

nubBy' (y : ys) xs = nubBy'2 (y : ys) xs

nubBy'0 y ys xs True = y : nubBy' ys (y : xs)

nubBy'1 y ys xs True = nubBy' ys xs

nubBy'1 y ys xs False = nubBy'0 y ys xs otherwise

nubBy'2 (y : ys) xs = nubBy'1 y ys xs (elem_by eq y xs)

nubBy'3 [] vy = []

nubBy'3 xv xw = nubBy'2 xv xw

are unpacked to the following functions on top level

nubByNubBy'1 xx y ys xs True = nubByNubBy' xx ys xs

nubByNubBy'1 xx y ys xs False = nubByNubBy'0 xx y ys xs otherwise

nubByNubBy'3 xx [] vy = []

nubByNubBy'3 xx xv xw = nubByNubBy'2 xx xv xw

nubByNubBy'2 xx (y : ys) xs = nubByNubBy'1 xx y ys xs (elem_by xx y xs)

nubByNubBy'0 xx y ys xs True = y : nubByNubBy' xx ys (y : xs)

nubByNubBy' xx [] vy = nubByNubBy'3 xx [] vy

nubByNubBy' xx (y : ys) xs = nubByNubBy'2 xx (y : ys) xs

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

mainModule List

(union :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	vw vx []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool

elem_by	vz wu []	=	False
elem_by	eq y (x : xs)	=	x `eq` y \|\| elem_by eq y xs

nubBy :: (a -> a -> Bool) -> [a] -> [a]

nubBy

eq l

nubByNubBy' eq l []

nubByNubBy'	xx [] vy	=	nubByNubBy'3 xx [] vy
nubByNubBy'	xx (y : ys) xs	=	nubByNubBy'2 xx (y : ys) xs

nubByNubBy'0

xx y ys xs True

y : nubByNubBy' xx ys (y : xs)

nubByNubBy'1	xx y ys xs True	=	nubByNubBy' xx ys xs
nubByNubBy'1	xx y ys xs False	=	nubByNubBy'0 xx y ys xs otherwise

nubByNubBy'2

xx (y : ys) xs

nubByNubBy'1 xx y ys xs (elem_by xx y xs)

nubByNubBy'3	xx [] vy	=	[]
nubByNubBy'3	xx xv xw	=	nubByNubBy'2 xx xv xw

union :: Eq a => [a] -> [a] -> [a]

union

unionBy (==)

unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

unionBy

eq xs ys

xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="union",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="union xy3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="union xy3 xy4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="unionBy (==) xy3 xy4",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="xy3 ++ foldl (flip (deleteBy (==))) (nubBy (==) xy4) xy3",fontsize=16,color="burlywood",shape="box"];6229[label="xy3/xy30 : xy31",fontsize=10,color="white",style="solid",shape="box"];6 -> 6229[label="",style="solid", color="burlywood", weight=9];
6229 -> 7[label="",style="solid", color="burlywood", weight=3];
6230[label="xy3/[]",fontsize=10,color="white",style="solid",shape="box"];6 -> 6230[label="",style="solid", color="burlywood", weight=9];
6230 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="(xy30 : xy31) ++ foldl (flip (deleteBy (==))) (nubBy (==) xy4) (xy30 : xy31)",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="[] ++ foldl (flip (deleteBy (==))) (nubBy (==) xy4) []",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="xy30 : xy31 ++ foldl (flip (deleteBy (==))) (nubBy (==) xy4) (xy30 : xy31)",fontsize=16,color="green",shape="box"];9 -> 11[label="",style="dashed", color="green", weight=3];
10[label="foldl (flip (deleteBy (==))) (nubBy (==) xy4) []",fontsize=16,color="black",shape="box"];10 -> 12[label="",style="solid", color="black", weight=3];
11 -> 168[label="",style="dashed", color="red", weight=0];
11[label="xy31 ++ foldl (flip (deleteBy (==))) (nubBy (==) xy4) (xy30 : xy31)",fontsize=16,color="magenta"];11 -> 169[label="",style="dashed", color="magenta", weight=3];
11 -> 170[label="",style="dashed", color="magenta", weight=3];
11 -> 171[label="",style="dashed", color="magenta", weight=3];
11 -> 172[label="",style="dashed", color="magenta", weight=3];
12[label="nubBy (==) xy4",fontsize=16,color="black",shape="triangle"];12 -> 15[label="",style="solid", color="black", weight=3];
169[label="xy31",fontsize=16,color="green",shape="box"];170 -> 12[label="",style="dashed", color="red", weight=0];
170[label="nubBy (==) xy4",fontsize=16,color="magenta"];171[label="xy31",fontsize=16,color="green",shape="box"];172[label="xy30",fontsize=16,color="green",shape="box"];168[label="xy8 ++ foldl (flip (deleteBy (==))) xy9 (xy10 : xy11)\n  Eq a",fontsize=16,color="burlywood",shape="triangle"];6233[label="xy8/xy80 : xy81",fontsize=10,color="white",style="solid",shape="box"];168 -> 6233[label="",style="solid", color="burlywood", weight=9];
6233 -> 197[label="",style="solid", color="burlywood", weight=3];
6234[label="xy8/[]",fontsize=10,color="white",style="solid",shape="box"];168 -> 6234[label="",style="solid", color="burlywood", weight=9];
6234 -> 198[label="",style="solid", color="burlywood", weight=3];
15[label="nubByNubBy' (==) xy4 []",fontsize=16,color="burlywood",shape="box"];6235[label="xy4/xy40 : xy41",fontsize=10,color="white",style="solid",shape="box"];15 -> 6235[label="",style="solid", color="burlywood", weight=9];
6235 -> 18[label="",style="solid", color="burlywood", weight=3];
6236[label="xy4/[]",fontsize=10,color="white",style="solid",shape="box"];15 -> 6236[label="",style="solid", color="burlywood", weight=9];
6236 -> 19[label="",style="solid", color="burlywood", weight=3];
197[label="(xy80 : xy81) ++ foldl (flip (deleteBy (==))) xy9 (xy10 : xy11)\n  Eq a",fontsize=16,color="black",shape="box"];197 -> 207[label="",style="solid", color="black", weight=3];
198[label="[] ++ foldl (flip (deleteBy (==))) xy9 (xy10 : xy11)\n  Eq a",fontsize=16,color="black",shape="box"];198 -> 208[label="",style="solid", color="black", weight=3];
18[label="nubByNubBy' (==) (xy40 : xy41) []",fontsize=16,color="black",shape="box"];18 -> 23[label="",style="solid", color="black", weight=3];
19[label="nubByNubBy' (==) [] []",fontsize=16,color="black",shape="box"];19 -> 24[label="",style="solid", color="black", weight=3];
207[label="xy80 : xy81 ++ foldl (flip (deleteBy (==))) xy9 (xy10 : xy11)\n  Eq a",fontsize=16,color="green",shape="box"];207 -> 223[label="",style="dashed", color="green", weight=3];
208[label="foldl (flip (deleteBy (==))) xy9 (xy10 : xy11)\n  Eq a",fontsize=16,color="black",shape="box"];208 -> 224[label="",style="solid", color="black", weight=3];
23[label="nubByNubBy'2 (==) (xy40 : xy41) []",fontsize=16,color="black",shape="box"];23 -> 28[label="",style="solid", color="black", weight=3];
24[label="nubByNubBy'3 (==) [] []",fontsize=16,color="black",shape="box"];24 -> 29[label="",style="solid", color="black", weight=3];
223 -> 168[label="",style="dashed", color="red", weight=0];
223[label="xy81 ++ foldl (flip (deleteBy (==))) xy9 (xy10 : xy11)\n  Eq a",fontsize=16,color="magenta"];223 -> 239[label="",style="dashed", color="magenta", weight=3];
224[label="foldl (flip (deleteBy (==))) (flip (deleteBy (==)) xy9 xy10) xy11\n  Eq a",fontsize=16,color="burlywood",shape="triangle"];6238[label="xy11/xy110 : xy111",fontsize=10,color="white",style="solid",shape="box"];224 -> 6238[label="",style="solid", color="burlywood", weight=9];
6238 -> 240[label="",style="solid", color="burlywood", weight=3];
6239[label="xy11/[]",fontsize=10,color="white",style="solid",shape="box"];224 -> 6239[label="",style="solid", color="burlywood", weight=9];
6239 -> 241[label="",style="solid", color="burlywood", weight=3];
28[label="nubByNubBy'1 (==) xy40 xy41 [] (elem_by (==) xy40 [])",fontsize=16,color="black",shape="box"];28 -> 33[label="",style="solid", color="black", weight=3];
29[label="[]",fontsize=16,color="green",shape="box"];239[label="xy81\n  Eq a",fontsize=16,color="green",shape="box"];240[label="foldl (flip (deleteBy (==))) (flip (deleteBy (==)) xy9 xy10) (xy110 : xy111)\n  Eq a",fontsize=16,color="black",shape="box"];240 -> 258[label="",style="solid", color="black", weight=3];
241[label="foldl (flip (deleteBy (==))) (flip (deleteBy (==)) xy9 xy10) []\n  Eq a",fontsize=16,color="black",shape="box"];241 -> 259[label="",style="solid", color="black", weight=3];
33[label="nubByNubBy'1 (==) xy40 xy41 [] False",fontsize=16,color="black",shape="box"];33 -> 37[label="",style="solid", color="black", weight=3];
258 -> 224[label="",style="dashed", color="red", weight=0];
258[label="foldl (flip (deleteBy (==))) (flip (deleteBy (==)) (flip (deleteBy (==)) xy9 xy10) xy110) xy111\n  Eq a",fontsize=16,color="magenta"];258 -> 280[label="",style="dashed", color="magenta", weight=3];
258 -> 281[label="",style="dashed", color="magenta", weight=3];
258 -> 282[label="",style="dashed", color="magenta", weight=3];
259[label="flip (deleteBy (==)) xy9 xy10\n  Eq a",fontsize=16,color="black",shape="triangle"];259 -> 283[label="",style="solid", color="black", weight=3];
37[label="nubByNubBy'0 (==) xy40 xy41 [] otherwise",fontsize=16,color="black",shape="box"];37 -> 42[label="",style="solid", color="black", weight=3];
280[label="xy111\n  Eq a",fontsize=16,color="green",shape="box"];281 -> 259[label="",style="dashed", color="red", weight=0];
281[label="flip (deleteBy (==)) xy9 xy10\n  Eq a",fontsize=16,color="magenta"];282[label="xy110\n  Eq a",fontsize=16,color="green",shape="box"];283[label="deleteBy (==) xy10 xy9\n  Eq a",fontsize=16,color="burlywood",shape="triangle"];6242[label="xy9/xy90 : xy91",fontsize=10,color="white",style="solid",shape="box"];283 -> 6242[label="",style="solid", color="burlywood", weight=9];
6242 -> 304[label="",style="solid", color="burlywood", weight=3];
6243[label="xy9/[]",fontsize=10,color="white",style="solid",shape="box"];283 -> 6243[label="",style="solid", color="burlywood", weight=9];
6243 -> 305[label="",style="solid", color="burlywood", weight=3];
42[label="nubByNubBy'0 (==) xy40 xy41 [] True",fontsize=16,color="black",shape="box"];42 -> 49[label="",style="solid", color="black", weight=3];
304[label="deleteBy (==) xy10 (xy90 : xy91)\n  Eq a",fontsize=16,color="black",shape="box"];304 -> 328[label="",style="solid", color="black", weight=3];
305[label="deleteBy (==) xy10 []\n  Eq a",fontsize=16,color="black",shape="box"];305 -> 329[label="",style="solid", color="black", weight=3];
49[label="xy40 : nubByNubBy' (==) xy41 (xy40 : [])",fontsize=16,color="green",shape="box"];49 -> 54[label="",style="dashed", color="green", weight=3];
328 -> 356[label="",style="dashed", color="red", weight=0];
328[label="deleteBy0 xy91 xy90 (==) xy10 ((==) xy10 xy90)\n  Eq a",fontsize=16,color="magenta"];328 -> 357[label="",style="dashed", color="magenta", weight=3];
328 -> 358[label="",style="dashed", color="magenta", weight=3];
328 -> 359[label="",style="dashed", color="magenta", weight=3];
328 -> 360[label="",style="dashed", color="magenta", weight=3];
329[label="[]\n  Eq a",fontsize=16,color="green",shape="box"];54[label="nubByNubBy' (==) xy41 (xy40 : [])",fontsize=16,color="burlywood",shape="box"];6245[label="xy41/xy410 : xy411",fontsize=10,color="white",style="solid",shape="box"];54 -> 6245[label="",style="solid", color="burlywood", weight=9];
6245 -> 59[label="",style="solid", color="burlywood", weight=3];
6246[label="xy41/[]",fontsize=10,color="white",style="solid",shape="box"];54 -> 6246[label="",style="solid", color="burlywood", weight=9];
6246 -> 60[label="",style="solid", color="burlywood", weight=3];
357[label="xy90\n  Eq a",fontsize=16,color="green",shape="box"];358[label="xy91\n  Eq a",fontsize=16,color="green",shape="box"];359[label="xy10\n  Eq a",fontsize=16,color="green",shape="box"];360[label="(==) xy10 xy90\n  Eq a",fontsize=16,color="blue",shape="box"];6247[label="== :: () -> () -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6247[label="",style="solid", color="blue", weight=9];
6247 -> 361[label="",style="solid", color="blue", weight=3];
6248[label="== :: Bool -> Bool -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6248[label="",style="solid", color="blue", weight=9];
6248 -> 362[label="",style="solid", color="blue", weight=3];
6249[label="== :: Integer -> Integer -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6249[label="",style="solid", color="blue", weight=9];
6249 -> 363[label="",style="solid", color="blue", weight=3];
6250[label="== :: ([] a) -> ([] a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6250[label="",style="solid", color="blue", weight=9];
6250 -> 364[label="",style="solid", color="blue", weight=3];
6251[label="== :: Char -> Char -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6251[label="",style="solid", color="blue", weight=9];
6251 -> 365[label="",style="solid", color="blue", weight=3];
6252[label="== :: (Either a b) -> (Either a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6252[label="",style="solid", color="blue", weight=9];
6252 -> 366[label="",style="solid", color="blue", weight=3];
6253[label="== :: Float -> Float -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6253[label="",style="solid", color="blue", weight=9];
6253 -> 367[label="",style="solid", color="blue", weight=3];
6254[label="== :: Double -> Double -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6254[label="",style="solid", color="blue", weight=9];
6254 -> 368[label="",style="solid", color="blue", weight=3];
6255[label="== :: ((@3) a b c) -> ((@3) a b c) -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6255[label="",style="solid", color="blue", weight=9];
6255 -> 369[label="",style="solid", color="blue", weight=3];
6256[label="== :: ((@2) a b) -> ((@2) a b) -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6256[label="",style="solid", color="blue", weight=9];
6256 -> 370[label="",style="solid", color="blue", weight=3];
6257[label="== :: Ordering -> Ordering -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6257[label="",style="solid", color="blue", weight=9];
6257 -> 371[label="",style="solid", color="blue", weight=3];
6258[label="== :: (Ratio a) -> (Ratio a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6258[label="",style="solid", color="blue", weight=9];
6258 -> 372[label="",style="solid", color="blue", weight=3];
6259[label="== :: Int -> Int -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6259[label="",style="solid", color="blue", weight=9];
6259 -> 373[label="",style="solid", color="blue", weight=3];
6260[label="== :: (Maybe a) -> (Maybe a) -> Bool",fontsize=10,color="white",style="solid",shape="box"];360 -> 6260[label="",style="solid", color="blue", weight=9];
6260 -> 374[label="",style="solid", color="blue", weight=3];
356[label="deleteBy0 xy17 xy18 (==) xy19 xy20\n  Eq a",fontsize=16,color="burlywood",shape="triangle"];6261[label="xy20/False",fontsize=10,color="white",style="solid",shape="box"];356 -> 6261[label="",style="solid", color="burlywood", weight=9];
6261 -> 375[label="",style="solid", color="burlywood", weight=3];
6262[label="xy20/True",fontsize=10,color="white",style="solid",shape="box"];356 -> 6262[label="",style="solid", color="burlywood", weight=9];
6262 -> 376[label="",style="solid", color="burlywood", weight=3];
59[label="nubByNubBy' (==) (xy410 : xy411) (xy40 : [])",fontsize=16,color="black",shape="box"];59 -> 70[label="",style="solid", color="black", weight=3];
60[label="nubByNubBy' (==) [] (xy40 : [])",fontsize=16,color="black",shape="box"];60 -> 71[label="",style="solid", color="black", weight=3];
361[label="(==) xy10 xy90",fontsize=16,color="black",shape="box"];361 -> 405[label="",style="solid", color="black", weight=3];
362[label="(==) xy10 xy90",fontsize=16,color="black",shape="box"];362 -> 406[label="",style="solid", color="black", weight=3];
363[label="(==) xy10 xy90",fontsize=16,color="black",shape="box"];363 -> 407[label="",style="solid", color="black", weight=3];
364[label="(==) xy10 xy90\n  Eq a",fontsize=16,color="black",shape="box"];364 -> 408[label="",style="solid", color="black", weight=3];
365[label="(==) xy10 xy90",fontsize=16,color="black",shape="box"];365 -> 409[label="",style="solid", color="black", weight=3];
366[label="(==) xy10 xy90\n  Eq a  Eq b",fontsize=16,color="black",shape="box"];366 -> 410[label="",style="solid", color="black", weight=3];
367[label="(==) xy10 xy90",fontsize=16,color="black",shape="box"];367 -> 411[label="",style="solid", color="black", weight=3];
368[label="(==) xy10 xy90",fontsize=16,color="black",shape="box"];368 -> 412[label="",style="solid", color="black", weight=3];
369[label="(==) xy10 xy90\n  Eq a  Eq b  Eq c",fontsize=16,color="black",shape="box"];369 -> 413[label="",style="solid", color="black", weight=3];
370[label="(==) xy10 xy90\n  Eq a  Eq b",fontsize=16,color="black",shape="box"];370 -> 414[label="",style="solid", color="black", weight=3];
371[label="(==) xy10 xy90",fontsize=16,color="black",shape="box"];371 -> 415[label="",style="solid", color="black", weight=3];
372[label="(==) xy10 xy90\n  Integral a",fontsize=16,color="black",shape="box"];372 -> 416[label="",style="solid", color="black", weight=3];
373[label="(==) xy10 xy90",fontsize=16,color="black",shape="box"];373 -> 417[label="",style="solid", color="black", weight=3];
374[label="(==) xy10 xy90\n  Eq a",fontsize=16,color="black",shape="box"];374 -> 418[label="",style="solid", color="black", weight=3];
375[label="deleteBy0 xy17 xy18 (==) xy19 False\n  Eq a",fontsize=16,color="black",shape="box"];375 -> 419[label="",style="solid", color="black", weight=3];
376[label="deleteBy0 xy17 xy18 (==) xy19 True\n  Eq a",fontsize=16,color="black",shape="box"];376 -> 420[label="",style="solid", color="black", weight=3];
70[label="nubByNubBy'2 (==) (xy410 : xy411) (xy40 : [])",fontsize=16,color="black",shape="box"];70 -> 83[label="",style="solid", color="black", weight=3];
71[label="nubByNubBy'3 (==) [] (xy40 : [])",fontsize=16,color="black",shape="box"];71 -> 84[label="",style="solid", color="black", weight=3];
405[label="error []",fontsize=16,color="red",shape="box"];406[label="error []",fontsize=16,color="red",shape="box"];407[label="error []",fontsize=16,color="red",shape="box"];408[label="error []",fontsize=16,color="red",shape="box"];409[label="error []",fontsize=16,color="red",shape="box"];410[label="error []",fontsize=16,color="red",shape="box"];411[label="error []",fontsize=16,color="red",shape="box"];412[label="error []",fontsize=16,color="red",shape="box"];413[label="error []",fontsize=16,color="red",shape="box"];414[label="error []",fontsize=16,color="red",shape="box"];415[label="error []",fontsize=16,color="red",shape="box"];416[label="error []",fontsize=16,color="red",shape="box"];417[label="primEqInt xy10 xy90",fontsize=16,color="burlywood",shape="triangle"];6263[label="xy10/Pos xy100",fontsize=10,color="white",style="solid",shape="box"];417 -> 6263[label="",style="solid", color="burlywood", weight=9];
6263 -> 461[label="",style="solid", color="burlywood", weight=3];
6264[label="xy10/Neg xy100",fontsize=10,color="white",style="solid",shape="box"];417 -> 6264[label="",style="solid", color="burlywood", weight=9];
6264 -> 462[label="",style="solid", color="burlywood", weight=3];
418[label="error []",fontsize=16,color="red",shape="box"];419[label="xy18 : deleteBy (==) xy19 xy17\n  Eq a",fontsize=16,color="green",shape="box"];419 -> 463[label="",style="dashed", color="green", weight=3];
420[label="xy17\n  Eq a",fontsize=16,color="green",shape="box"];83[label="nubByNubBy'1 (==) xy410 xy411 (xy40 : []) (elem_by (==) xy410 (xy40 : []))",fontsize=16,color="black",shape="box"];83 -> 101[label="",style="solid", color="black", weight=3];
84[label="[]",fontsize=16,color="green",shape="box"];461[label="primEqInt (Pos xy100) xy90",fontsize=16,color="burlywood",shape="box"];6265[label="xy100/Succ xy1000",fontsize=10,color="white",style="solid",shape="box"];461 -> 6265[label="",style="solid", color="burlywood", weight=9];
6265 -> 502[label="",style="solid", color="burlywood", weight=3];
6266[label="xy100/Zero",fontsize=10,color="white",style="solid",shape="box"];461 -> 6266[label="",style="solid", color="burlywood", weight=9];
6266 -> 503[label="",style="solid", color="burlywood", weight=3];
462[label="primEqInt (Neg xy100) xy90",fontsize=16,color="burlywood",shape="box"];6267[label="xy100/Succ xy1000",fontsize=10,color="white",style="solid",shape="box"];462 -> 6267[label="",style="solid", color="burlywood", weight=9];
6267 -> 504[label="",style="solid", color="burlywood", weight=3];
6268[label="xy100/Zero",fontsize=10,color="white",style="solid",shape="box"];462 -> 6268[label="",style="solid", color="burlywood", weight=9];
6268 -> 505[label="",style="solid", color="burlywood", weight=3];
463 -> 283[label="",style="dashed", color="red", weight=0];
463[label="deleteBy (==) xy19 xy17\n  Eq a",fontsize=16,color="magenta"];463 -> 506[label="",style="dashed", color="magenta", weight=3];
463 -> 507[label="",style="dashed", color="magenta", weight=3];
101[label="nubByNubBy'1 (==) xy410 xy411 (xy40 : []) ((==) xy40 xy410 || elem_by (==) xy410 [])",fontsize=16,color="black",shape="box"];101 -> 122[label="",style="solid", color="black", weight=3];
502[label="primEqInt (Pos (Succ xy1000)) xy90",fontsize=16,color="burlywood",shape="box"];6270[label="xy90/Pos xy900",fontsize=10,color="white",style="solid",shape="box"];502 -> 6270[label="",style="solid", color="burlywood", weight=9];
6270 -> 544[label="",style="solid", color="burlywood", weight=3];
6271[label="xy90/Neg xy900",fontsize=10,color="white",style="solid",shape="box"];502 -> 6271[label="",style="solid", color="burlywood", weight=9];
6271 -> 545[label="",style="solid", color="burlywood", weight=3];
503[label="primEqInt (Pos Zero) xy90",fontsize=16,color="burlywood",shape="box"];6272[label="xy90/Pos xy900",fontsize=10,color="white",style="solid",shape="box"];503 -> 6272[label="",style="solid", color="burlywood", weight=9];
6272 -> 546[label="",style="solid", color="burlywood", weight=3];
6273[label="xy90/Neg xy900",fontsize=10,color="white",style="solid",shape="box"];503 -> 6273[label="",style="solid", color="burlywood", weight=9];
6273 -> 547[label="",style="solid", color="burlywood", weight=3];
504[label="primEqInt (Neg (Succ xy1000)) xy90",fontsize=16,color="burlywood",shape="box"];6274[label="xy90/Pos xy900",fontsize=10,color="white",style="solid",shape="box"];504 -> 6274[label="",style="solid", color="burlywood", weight=9];
6274 -> 548[label="",style="solid", color="burlywood", weight=3];
6275[label="xy90/Neg xy900",fontsize=10,color="white",style="solid",shape="box"];504 -> 6275[label="",style="solid", color="burlywood", weight=9];
6275 -> 549[label="",style="solid", color="burlywood", weight=3];
505[label="primEqInt (Neg Zero) xy90",fontsize=16,color="burlywood",shape="box"];6276[label="xy90/Pos xy900",fontsize=10,color="white",style="solid",shape="box"];505 -> 6276[label="",style="solid", color="burlywood", weight=9];
6276 -> 550[label="",style="solid", color="burlywood", weight=3];
6277[label="xy90/Neg xy900",fontsize=10,color="white",style="solid",shape="box"];505 -> 6277[label="",style="solid", color="burlywood", weight=9];
6277 -> 551[label="",style="solid", color="burlywood", weight=3];
506[label="xy17\n  Eq a",fontsize=16,color="green",shape="box"];507[label="xy19\n  Eq a",fontsize=16,color="green",shape="box"];122 -> 6191[label="",style="dashed", color="red", weight=0];
122[label="nubByNubBy'1 primEqInt xy410 xy411 (xy40 : []) (primEqInt xy40 xy410 || elem_by primEqInt xy410 [])",fontsize=16,color="magenta"];122 -> 6192[label="",style="dashed", color="magenta", weight=3];
122 -> 6193[label="",style="dashed", color="magenta", weight=3];
122 -> 6194[label="",style="dashed", color="magenta", weight=3];
122 -> 6195[label="",style="dashed", color="magenta", weight=3];
122 -> 6196[label="",style="dashed", color="magenta", weight=3];
122 -> 6197[label="",style="dashed", color="magenta", weight=3];
544[label="primEqInt (Pos (Succ xy1000)) (Pos xy900)",fontsize=16,color="burlywood",shape="box"];6279[label="xy900/Succ xy9000",fontsize=10,color="white",style="solid",shape="box"];544 -> 6279[label="",style="solid", color="burlywood", weight=9];
6279 -> 571[label="",style="solid", color="burlywood", weight=3];
6280[label="xy900/Zero",fontsize=10,color="white",style="solid",shape="box"];544 -> 6280[label="",style="solid", color="burlywood", weight=9];
6280 -> 572[label="",style="solid", color="burlywood", weight=3];
545[label="primEqInt (Pos (Succ xy1000)) (Neg xy900)",fontsize=16,color="black",shape="box"];545 -> 573[label="",style="solid", color="black", weight=3];
546[label="primEqInt (Pos Zero) (Pos xy900)",fontsize=16,color="burlywood",shape="box"];6281[label="xy900/Succ xy9000",fontsize=10,color="white",style="solid",shape="box"];546 -> 6281[label="",style="solid", color="burlywood", weight=9];
6281 -> 574[label="",style="solid", color="burlywood", weight=3];
6282[label="xy900/Zero",fontsize=10,color="white",style="solid",shape="box"];546 -> 6282[label="",style="solid", color="burlywood", weight=9];
6282 -> 575[label="",style="solid", color="burlywood", weight=3];
547[label="primEqInt (Pos Zero) (Neg xy900)",fontsize=16,color="burlywood",shape="box"];6283[label="xy900/Succ xy9000",fontsize=10,color="white",style="solid",shape="box"];547 -> 6283[label="",style="solid", color="burlywood", weight=9];
6283 -> 576[label="",style="solid", color="burlywood", weight=3];
6284[label="xy900/Zero",fontsize=10,color="white",style="solid",shape="box"];547 -> 6284[label="",style="solid", color="burlywood", weight=9];
6284 -> 577[label="",style="solid", color="burlywood", weight=3];
548[label="primEqInt (Neg (Succ xy1000)) (Pos xy900)",fontsize=16,color="black",shape="box"];548 -> 578[label="",style="solid", color="black", weight=3];
549[label="primEqInt (Neg (Succ xy1000)) (Neg xy900)",fontsize=16,color="burlywood",shape="box"];6285[label="xy900/Succ xy9000",fontsize=10,color="white",style="solid",shape="box"];549 -> 6285[label="",style="solid", color="burlywood", weight=9];
6285 -> 579[label="",style="solid", color="burlywood", weight=3];
6286[label="xy900/Zero",fontsize=10,color="white",style="solid",shape="box"];549 -> 6286[label="",style="solid", color="burlywood", weight=9];
6286 -> 580[label="",style="solid", color="burlywood", weight=3];
550[label="primEqInt (Neg Zero) (Pos xy900)",fontsize=16,color="burlywood",shape="box"];6287[label="xy900/Succ xy9000",fontsize=10,color="white",style="solid",shape="box"];550 -> 6287[label="",style="solid", color="burlywood", weight=9];
6287 -> 581[label="",style="solid", color="burlywood", weight=3];
6288[label="xy900/Zero",fontsize=10,color="white",style="solid",shape="box"];550 -> 6288[label="",style="solid", color="burlywood", weight=9];
6288 -> 582[label="",style="solid", color="burlywood", weight=3];
551[label="primEqInt (Neg Zero) (Neg xy900)",fontsize=16,color="burlywood",shape="box"];6289[label="xy900/Succ xy9000",fontsize=10,color="white",style="solid",shape="box"];551 -> 6289[label="",style="solid", color="burlywood", weight=9];
6289 -> 583[label="",style="solid", color="burlywood", weight=3];
6290[label="xy900/Zero",fontsize=10,color="white",style="solid",shape="box"];551 -> 6290[label="",style="solid", color="burlywood", weight=9];
6290 -> 584[label="",style="solid", color="burlywood", weight=3];
6192[label="[]",fontsize=16,color="green",shape="box"];6193[label="[]",fontsize=16,color="green",shape="box"];6194[label="xy40",fontsize=16,color="green",shape="box"];6195 -> 417[label="",style="dashed", color="red", weight=0];
6195[label="primEqInt xy40 xy410",fontsize=16,color="magenta"];6195 -> 6199[label="",style="dashed", color="magenta", weight=3];
6195 -> 6200[label="",style="dashed", color="magenta", weight=3];
6196[label="xy411",fontsize=16,color="green",shape="box"];6197[label="xy410",fontsize=16,color="green",shape="box"];6191[label="nubByNubBy'1 primEqInt xy381 xy382 (xy383 : xy384) (xy387 || elem_by primEqInt xy381 xy386)",fontsize=16,color="burlywood",shape="triangle"];6292[label="xy387/False",fontsize=10,color="white",style="solid",shape="box"];6191 -> 6292[label="",style="solid", color="burlywood", weight=9];
6292 -> 6201[label="",style="solid", color="burlywood", weight=3];
6293[label="xy387/True",fontsize=10,color="white",style="solid",shape="box"];6191 -> 6293[label="",style="solid", color="burlywood", weight=9];
6293 -> 6202[label="",style="solid", color="burlywood", weight=3];
571[label="primEqInt (Pos (Succ xy1000)) (Pos (Succ xy9000))",fontsize=16,color="black",shape="box"];571 -> 589[label="",style="solid", color="black", weight=3];
572[label="primEqInt (Pos (Succ xy1000)) (Pos Zero)",fontsize=16,color="black",shape="box"];572 -> 590[label="",style="solid", color="black", weight=3];
573[label="False",fontsize=16,color="green",shape="box"];574[label="primEqInt (Pos Zero) (Pos (Succ xy9000))",fontsize=16,color="black",shape="box"];574 -> 591[label="",style="solid", color="black", weight=3];
575[label="primEqInt (Pos Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];575 -> 592[label="",style="solid", color="black", weight=3];
576[label="primEqInt (Pos Zero) (Neg (Succ xy9000))",fontsize=16,color="black",shape="box"];576 -> 593[label="",style="solid", color="black", weight=3];
577[label="primEqInt (Pos Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];577 -> 594[label="",style="solid", color="black", weight=3];
578[label="False",fontsize=16,color="green",shape="box"];579[label="primEqInt (Neg (Succ xy1000)) (Neg (Succ xy9000))",fontsize=16,color="black",shape="box"];579 -> 595[label="",style="solid", color="black", weight=3];
580[label="primEqInt (Neg (Succ xy1000)) (Neg Zero)",fontsize=16,color="black",shape="box"];580 -> 596[label="",style="solid", color="black", weight=3];
581[label="primEqInt (Neg Zero) (Pos (Succ xy9000))",fontsize=16,color="black",shape="box"];581 -> 597[label="",style="solid", color="black", weight=3];
582[label="primEqInt (Neg Zero) (Pos Zero)",fontsize=16,color="black",shape="box"];582 -> 598[label="",style="solid", color="black", weight=3];
583[label="primEqInt (Neg Zero) (Neg (Succ xy9000))",fontsize=16,color="black",shape="box"];583 -> 599[label="",style="solid", color="black", weight=3];
584[label="primEqInt (Neg Zero) (Neg Zero)",fontsize=16,color="black",shape="box"];584 -> 600[label="",style="solid", color="black", weight=3];
6199[label="xy410",fontsize=16,color="green",shape="box"];6200[label="xy40",fontsize=16,color="green",shape="box"];6201[label="nubByNubBy'1 primEqInt xy381 xy382 (xy383 : xy384) (False || elem_by primEqInt xy381 xy386)",fontsize=16,color="black",shape="box"];6201 -> 6203[label="",style="solid", color="black", weight=3];
6202[label="nubByNubBy'1 primEqInt xy381 xy382 (xy383 : xy384) (True || elem_by primEqInt xy381 xy386)",fontsize=16,color="black",shape="box"];6202 -> 6204[label="",style="solid", color="black", weight=3];
589[label="primEqNat xy1000 xy9000",fontsize=16,color="burlywood",shape="triangle"];6294[label="xy1000/Succ xy10000",fontsize=10,color="white",style="solid",shape="box"];589 -> 6294[label="",style="solid", color="burlywood", weight=9];
6294 -> 637[label="",style="solid", color="burlywood", weight=3];
6295[label="xy1000/Zero",fontsize=10,color="white",style="solid",shape="box"];589 -> 6295[label="",style="solid", color="burlywood", weight=9];
6295 -> 638[label="",style="solid", color="burlywood", weight=3];
590[label="False",fontsize=16,color="green",shape="box"];591[label="False",fontsize=16,color="green",shape="box"];592[label="True",fontsize=16,color="green",shape="box"];593[label="False",fontsize=16,color="green",shape="box"];594[label="True",fontsize=16,color="green",shape="box"];595 -> 589[label="",style="dashed", color="red", weight=0];
595[label="primEqNat xy1000 xy9000",fontsize=16,color="magenta"];595 -> 639[label="",style="dashed", color="magenta", weight=3];
595 -> 640[label="",style="dashed", color="magenta", weight=3];
596[label="False",fontsize=16,color="green",shape="box"];597[label="False",fontsize=16,color="green",shape="box"];598[label="True",fontsize=16,color="green",shape="box"];599[label="False",fontsize=16,color="green",shape="box"];600[label="True",fontsize=16,color="green",shape="box"];6203[label="nubByNubBy'1 primEqInt xy381 xy382 (xy383 : xy384) (elem_by primEqInt xy381 xy386)",fontsize=16,color="burlywood",shape="triangle"];6297[label="xy386/xy3860 : xy3861",fontsize=10,color="white",style="solid",shape="box"];6203 -> 6297[label="",style="solid", color="burlywood", weight=9];
6297 -> 6205[label="",style="solid", color="burlywood", weight=3];
6298[label="xy386/[]",fontsize=10,color="white",style="solid",shape="box"];6203 -> 6298[label="",style="solid", color="burlywood", weight=9];
6298 -> 6206[label="",style="solid", color="burlywood", weight=3];
6204[label="nubByNubBy'1 primEqInt xy381 xy382 (xy383 : xy384) True",fontsize=16,color="black",shape="box"];6204 -> 6207[label="",style="solid", color="black", weight=3];
637[label="primEqNat (Succ xy10000) xy9000",fontsize=16,color="burlywood",shape="box"];6299[label="xy9000/Succ xy90000",fontsize=10,color="white",style="solid",shape="box"];637 -> 6299[label="",style="solid", color="burlywood", weight=9];
6299 -> 647[label="",style="solid", color="burlywood", weight=3];
6300[label="xy9000/Zero",fontsize=10,color="white",style="solid",shape="box"];637 -> 6300[label="",style="solid", color="burlywood", weight=9];
6300 -> 648[label="",style="solid", color="burlywood", weight=3];
638[label="primEqNat Zero xy9000",fontsize=16,color="burlywood",shape="box"];6301[label="xy9000/Succ xy90000",fontsize=10,color="white",style="solid",shape="box"];638 -> 6301[label="",style="solid", color="burlywood", weight=9];
6301 -> 649[label="",style="solid", color="burlywood", weight=3];
6302[label="xy9000/Zero",fontsize=10,color="white",style="solid",shape="box"];638 -> 6302[label="",style="solid", color="burlywood", weight=9];
6302 -> 650[label="",style="solid", color="burlywood", weight=3];
639[label="xy9000",fontsize=16,color="green",shape="box"];640[label="xy1000",fontsize=16,color="green",shape="box"];6205[label="nubByNubBy'1 primEqInt xy381 xy382 (xy383 : xy384) (elem_by primEqInt xy381 (xy3860 : xy3861))",fontsize=16,color="black",shape="box"];6205 -> 6208[label="",style="solid", color="black", weight=3];
6206[label="nubByNubBy'1 primEqInt xy381 xy382 (xy383 : xy384) (elem_by primEqInt xy381 [])",fontsize=16,color="black",shape="box"];6206 -> 6209[label="",style="solid", color="black", weight=3];
6207[label="nubByNubBy' primEqInt xy382 (xy383 : xy384)",fontsize=16,color="burlywood",shape="triangle"];6303[label="xy382/xy3820 : xy3821",fontsize=10,color="white",style="solid",shape="box"];6207 -> 6303[label="",style="solid", color="burlywood", weight=9];
6303 -> 6210[label="",style="solid", color="burlywood", weight=3];
6304[label="xy382/[]",fontsize=10,color="white",style="solid",shape="box"];6207 -> 6304[label="",style="solid", color="burlywood", weight=9];
6304 -> 6211[label="",style="solid", color="burlywood", weight=3];
647[label="primEqNat (Succ xy10000) (Succ xy90000)",fontsize=16,color="black",shape="box"];647 -> 653[label="",style="solid", color="black", weight=3];
648[label="primEqNat (Succ xy10000) Zero",fontsize=16,color="black",shape="box"];648 -> 654[label="",style="solid", color="black", weight=3];
649[label="primEqNat Zero (Succ xy90000)",fontsize=16,color="black",shape="box"];649 -> 655[label="",style="solid", color="black", weight=3];
650[label="primEqNat Zero Zero",fontsize=16,color="black",shape="box"];650 -> 656[label="",style="solid", color="black", weight=3];
6208 -> 6191[label="",style="dashed", color="red", weight=0];
6208[label="nubByNubBy'1 primEqInt xy381 xy382 (xy383 : xy384) (primEqInt xy3860 xy381 || elem_by primEqInt xy381 xy3861)",fontsize=16,color="magenta"];6208 -> 6212[label="",style="dashed", color="magenta", weight=3];
6208 -> 6213[label="",style="dashed", color="magenta", weight=3];
6209[label="nubByNubBy'1 primEqInt xy381 xy382 (xy383 : xy384) False",fontsize=16,color="black",shape="box"];6209 -> 6214[label="",style="solid", color="black", weight=3];
6210[label="nubByNubBy' primEqInt (xy3820 : xy3821) (xy383 : xy384)",fontsize=16,color="black",shape="box"];6210 -> 6215[label="",style="solid", color="black", weight=3];
6211[label="nubByNubBy' primEqInt [] (xy383 : xy384)",fontsize=16,color="black",shape="box"];6211 -> 6216[label="",style="solid", color="black", weight=3];
653 -> 589[label="",style="dashed", color="red", weight=0];
653[label="primEqNat xy10000 xy90000",fontsize=16,color="magenta"];653 -> 678[label="",style="dashed", color="magenta", weight=3];
653 -> 679[label="",style="dashed", color="magenta", weight=3];
654[label="False",fontsize=16,color="green",shape="box"];655[label="False",fontsize=16,color="green",shape="box"];656[label="True",fontsize=16,color="green",shape="box"];6212[label="xy3861",fontsize=16,color="green",shape="box"];6213 -> 417[label="",style="dashed", color="red", weight=0];
6213[label="primEqInt xy3860 xy381",fontsize=16,color="magenta"];6213 -> 6217[label="",style="dashed", color="magenta", weight=3];
6213 -> 6218[label="",style="dashed", color="magenta", weight=3];
6214[label="nubByNubBy'0 primEqInt xy381 xy382 (xy383 : xy384) otherwise",fontsize=16,color="black",shape="box"];6214 -> 6219[label="",style="solid", color="black", weight=3];
6215[label="nubByNubBy'2 primEqInt (xy3820 : xy3821) (xy383 : xy384)",fontsize=16,color="black",shape="box"];6215 -> 6220[label="",style="solid", color="black", weight=3];
6216[label="nubByNubBy'3 primEqInt [] (xy383 : xy384)",fontsize=16,color="black",shape="box"];6216 -> 6221[label="",style="solid", color="black", weight=3];
678[label="xy90000",fontsize=16,color="green",shape="box"];679[label="xy10000",fontsize=16,color="green",shape="box"];6217[label="xy381",fontsize=16,color="green",shape="box"];6218[label="xy3860",fontsize=16,color="green",shape="box"];6219[label="nubByNubBy'0 primEqInt xy381 xy382 (xy383 : xy384) True",fontsize=16,color="black",shape="box"];6219 -> 6222[label="",style="solid", color="black", weight=3];
6220 -> 6203[label="",style="dashed", color="red", weight=0];
6220[label="nubByNubBy'1 primEqInt xy3820 xy3821 (xy383 : xy384) (elem_by primEqInt xy3820 (xy383 : xy384))",fontsize=16,color="magenta"];6220 -> 6223[label="",style="dashed", color="magenta", weight=3];
6220 -> 6224[label="",style="dashed", color="magenta", weight=3];
6220 -> 6225[label="",style="dashed", color="magenta", weight=3];
6221[label="[]",fontsize=16,color="green",shape="box"];6222[label="xy381 : nubByNubBy' primEqInt xy382 (xy381 : xy383 : xy384)",fontsize=16,color="green",shape="box"];6222 -> 6226[label="",style="dashed", color="green", weight=3];
6223[label="xy383 : xy384",fontsize=16,color="green",shape="box"];6224[label="xy3821",fontsize=16,color="green",shape="box"];6225[label="xy3820",fontsize=16,color="green",shape="box"];6226 -> 6207[label="",style="dashed", color="red", weight=0];
6226[label="nubByNubBy' primEqInt xy382 (xy381 : xy383 : xy384)",fontsize=16,color="magenta"];6226 -> 6227[label="",style="dashed", color="magenta", weight=3];
6226 -> 6228[label="",style="dashed", color="magenta", weight=3];
6227[label="xy383 : xy384",fontsize=16,color="green",shape="box"];6228[label="xy381",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xy10000), Succ(xy90000)) → new_primEqNat(xy10000, xy90000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primEqNat(Succ(xy10000), Succ(xy90000)) → new_primEqNat(xy10000, xy90000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_nubByNubBy'1(xy381, xy382, xy383, xy384, False, :(xy3860, xy3861)) → new_nubByNubBy'1(xy381, xy382, xy383, xy384, new_primEqInt(xy3860, xy381), xy3861)
new_nubByNubBy'10(xy381, xy382, xy383, xy384, []) → new_nubByNubBy'(xy382, xy381, :(xy383, xy384))
new_nubByNubBy'1(xy381, xy382, xy383, xy384, False, []) → new_nubByNubBy'(xy382, xy381, :(xy383, xy384))
new_nubByNubBy'10(xy381, xy382, xy383, xy384, :(xy3860, xy3861)) → new_nubByNubBy'1(xy381, xy382, xy383, xy384, new_primEqInt(xy3860, xy381), xy3861)
new_nubByNubBy'1(xy381, :(xy3820, xy3821), xy383, xy384, True, xy386) → new_nubByNubBy'10(xy3820, xy3821, xy383, xy384, :(xy383, xy384))
new_nubByNubBy'(:(xy3820, xy3821), xy383, xy384) → new_nubByNubBy'10(xy3820, xy3821, xy383, xy384, :(xy383, xy384))

The TRS R consists of the following rules:

new_primEqNat0(Succ(xy10000), Zero) → False
new_primEqNat0(Zero, Succ(xy90000)) → False
new_primEqInt(Neg(Zero), Pos(Succ(xy9000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy9000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Zero), Neg(Succ(xy9000))) → False
new_primEqInt(Neg(Succ(xy1000)), Neg(Zero)) → False
new_primEqNat0(Succ(xy10000), Succ(xy90000)) → new_primEqNat0(xy10000, xy90000)
new_primEqNat0(Zero, Zero) → True
new_primEqInt(Pos(Zero), Pos(Succ(xy9000))) → False
new_primEqInt(Pos(Succ(xy1000)), Pos(Zero)) → False
new_primEqInt(Neg(Succ(xy1000)), Pos(xy900)) → False
new_primEqInt(Pos(Succ(xy1000)), Neg(xy900)) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Pos(Succ(xy1000)), Pos(Succ(xy9000))) → new_primEqNat0(xy1000, xy9000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Succ(xy1000)), Neg(Succ(xy9000))) → new_primEqNat0(xy1000, xy9000)

The set Q consists of the following terms:

new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqNat0(Zero, Zero)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqNat0(Succ(x0), Zero)
new_primEqNat0(Zero, Succ(x0))
new_primEqNat0(Succ(x0), Succ(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_primEqInt(Neg(Zero), Neg(Zero))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_nubByNubBy'1(xy381, xy382, xy383, xy384, False, :(xy3860, xy3861)) → new_nubByNubBy'1(xy381, xy382, xy383, xy384, new_primEqInt(xy3860, xy381), xy3861)
new_nubByNubBy'1(xy381, xy382, xy383, xy384, False, []) → new_nubByNubBy'(xy382, xy381, :(xy383, xy384))
new_nubByNubBy'10(xy381, xy382, xy383, xy384, :(xy3860, xy3861)) → new_nubByNubBy'1(xy381, xy382, xy383, xy384, new_primEqInt(xy3860, xy381), xy3861)
new_nubByNubBy'1(xy381, :(xy3820, xy3821), xy383, xy384, True, xy386) → new_nubByNubBy'10(xy3820, xy3821, xy383, xy384, :(xy383, xy384))
new_nubByNubBy'(:(xy3820, xy3821), xy383, xy384) → new_nubByNubBy'10(xy3820, xy3821, xy383, xy384, :(xy383, xy384))

The TRS R consists of the following rules:

new_primEqNat0(Succ(xy10000), Zero) → False
new_primEqNat0(Zero, Succ(xy90000)) → False
new_primEqInt(Neg(Zero), Pos(Succ(xy9000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy9000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Zero), Neg(Succ(xy9000))) → False
new_primEqInt(Neg(Succ(xy1000)), Neg(Zero)) → False
new_primEqNat0(Succ(xy10000), Succ(xy90000)) → new_primEqNat0(xy10000, xy90000)
new_primEqNat0(Zero, Zero) → True
new_primEqInt(Pos(Zero), Pos(Succ(xy9000))) → False
new_primEqInt(Pos(Succ(xy1000)), Pos(Zero)) → False
new_primEqInt(Neg(Succ(xy1000)), Pos(xy900)) → False
new_primEqInt(Pos(Succ(xy1000)), Neg(xy900)) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Pos(Succ(xy1000)), Pos(Succ(xy9000))) → new_primEqNat0(xy1000, xy9000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Succ(xy1000)), Neg(Succ(xy9000))) → new_primEqNat0(xy1000, xy9000)

The set Q consists of the following terms:

new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqNat0(Zero, Zero)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqNat0(Succ(x0), Zero)
new_primEqNat0(Zero, Succ(x0))
new_primEqNat0(Succ(x0), Succ(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_primEqInt(Neg(Zero), Neg(Zero))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_nubByNubBy'(:(xy3820, xy3821), xy383, xy384) → new_nubByNubBy'10(xy3820, xy3821, xy383, xy384, :(xy383, xy384))
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3, 3 >= 4
new_nubByNubBy'10(xy381, xy382, xy383, xy384, :(xy3860, xy3861)) → new_nubByNubBy'1(xy381, xy382, xy383, xy384, new_primEqInt(xy3860, xy381), xy3861)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 > 6
new_nubByNubBy'1(xy381, xy382, xy383, xy384, False, :(xy3860, xy3861)) → new_nubByNubBy'1(xy381, xy382, xy383, xy384, new_primEqInt(xy3860, xy381), xy3861)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 6 > 6
new_nubByNubBy'1(xy381, xy382, xy383, xy384, False, []) → new_nubByNubBy'(xy382, xy381, :(xy383, xy384))
The graph contains the following edges 2 >= 1, 1 >= 2
new_nubByNubBy'1(xy381, :(xy3820, xy3821), xy383, xy384, True, xy386) → new_nubByNubBy'10(xy3820, xy3821, xy383, xy384, :(xy383, xy384))
The graph contains the following edges 2 > 1, 2 > 2, 3 >= 3, 4 >= 4

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy(xy10, :(xy90, xy91), bb) → new_deleteBy0(xy91, xy90, xy10, new_esEs(xy10, xy90, bb), bb)
new_deleteBy0(xy17, xy18, xy19, False, ba) → new_deleteBy(xy19, xy17, ba)

The TRS R consists of the following rules:

new_esEs(xy10, xy90, ty_Ordering) → error([])
new_esEs(xy10, xy90, ty_@0) → error([])
new_esEs(xy10, xy90, app(ty_Ratio, cc)) → error([])
new_esEs(xy10, xy90, ty_Char) → error([])
new_primEqInt(Neg(Succ(xy1000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xy9000))) → False
new_esEs(xy10, xy90, ty_Bool) → error([])
new_primEqNat0(Succ(xy10000), Succ(xy90000)) → new_primEqNat0(xy10000, xy90000)
new_primEqNat0(Zero, Zero) → True
new_primEqInt(Pos(Succ(xy1000)), Neg(xy900)) → False
new_primEqInt(Neg(Succ(xy1000)), Pos(xy900)) → False
new_esEs(xy10, xy90, app(app(ty_Either, bd), be)) → error([])
new_esEs(xy10, xy90, ty_Int) → new_primEqInt(xy10, xy90)
new_primEqInt(Neg(Succ(xy1000)), Neg(Succ(xy9000))) → new_primEqNat0(xy1000, xy9000)
new_esEs(xy10, xy90, app(app(app(ty_@3, bf), bg), bh)) → error([])
new_esEs(xy10, xy90, ty_Double) → error([])
new_primEqNat0(Succ(xy10000), Zero) → False
new_primEqNat0(Zero, Succ(xy90000)) → False
new_esEs(xy10, xy90, ty_Integer) → error([])
new_primEqInt(Pos(Zero), Neg(Succ(xy9000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xy9000))) → False
new_esEs(xy10, xy90, app(app(ty_@2, ca), cb)) → error([])
new_esEs(xy10, xy90, app(ty_[], bc)) → error([])
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Succ(xy1000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy9000))) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs(xy10, xy90, ty_Float) → error([])
new_primEqInt(Pos(Succ(xy1000)), Pos(Succ(xy9000))) → new_primEqNat0(xy1000, xy9000)
new_esEs(xy10, xy90, app(ty_Maybe, cd)) → error([])
new_primEqInt(Neg(Zero), Neg(Zero)) → True

The set Q consists of the following terms:

new_esEs(x0, x1, ty_Integer)
new_esEs(x0, x1, ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs(x0, x1, ty_Ordering)
new_esEs(x0, x1, ty_Int)
new_primEqNat0(Zero, Succ(x0))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs(x0, x1, app(ty_Maybe, x2))
new_esEs(x0, x1, app(app(ty_Either, x2), x3))
new_esEs(x0, x1, ty_Double)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqNat0(Zero, Zero)
new_primEqNat0(Succ(x0), Zero)
new_esEs(x0, x1, ty_Bool)
new_esEs(x0, x1, ty_Char)
new_esEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_primEqNat0(Succ(x0), Succ(x1))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs(x0, x1, app(ty_[], x2))
new_esEs(x0, x1, app(app(ty_@2, x2), x3))
new_esEs(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_deleteBy0(xy17, xy18, xy19, False, ba) → new_deleteBy(xy19, xy17, ba)
The graph contains the following edges 3 >= 1, 1 >= 2, 5 >= 3
new_deleteBy(xy10, :(xy90, xy91), bb) → new_deleteBy0(xy91, xy90, xy10, new_esEs(xy10, xy90, bb), bb)
The graph contains the following edges 2 > 1, 2 > 2, 1 >= 3, 3 >= 5

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldl(xy9, xy10, :(xy110, xy111), ba) → new_foldl(new_flip(xy9, xy10, ba), xy110, xy111, ba)

The TRS R consists of the following rules:

new_esEs(xy10, xy90, ty_Ordering) → error([])
new_esEs(xy10, xy90, ty_@0) → error([])
new_esEs(xy10, xy90, app(ty_Ratio, cb)) → error([])
new_deleteBy00(xy17, xy18, xy19, True, cd) → xy17
new_esEs(xy10, xy90, ty_Char) → error([])
new_primEqInt(Neg(Zero), Neg(Succ(xy9000))) → False
new_primEqInt(Neg(Succ(xy1000)), Neg(Zero)) → False
new_esEs(xy10, xy90, ty_Bool) → error([])
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(xy10000), Succ(xy90000)) → new_primEqNat0(xy10000, xy90000)
new_primEqInt(Pos(Succ(xy1000)), Neg(xy900)) → False
new_primEqInt(Neg(Succ(xy1000)), Pos(xy900)) → False
new_esEs(xy10, xy90, app(app(ty_Either, bc), bd)) → error([])
new_esEs(xy10, xy90, ty_Int) → new_primEqInt(xy10, xy90)
new_primEqInt(Neg(Succ(xy1000)), Neg(Succ(xy9000))) → new_primEqNat0(xy1000, xy9000)
new_deleteBy1(xy10, [], ba) → []
new_esEs(xy10, xy90, ty_Double) → error([])
new_esEs(xy10, xy90, app(app(app(ty_@3, be), bf), bg)) → error([])
new_primEqNat0(Zero, Succ(xy90000)) → False
new_primEqNat0(Succ(xy10000), Zero) → False
new_esEs(xy10, xy90, ty_Integer) → error([])
new_primEqInt(Pos(Zero), Neg(Succ(xy9000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xy9000))) → False
new_esEs(xy10, xy90, app(ty_[], bb)) → error([])
new_esEs(xy10, xy90, app(app(ty_@2, bh), ca)) → error([])
new_deleteBy00(xy17, xy18, xy19, False, cd) → :(xy18, new_deleteBy1(xy19, xy17, cd))
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_deleteBy1(xy10, :(xy90, xy91), ba) → new_deleteBy00(xy91, xy90, xy10, new_esEs(xy10, xy90, ba), ba)
new_primEqInt(Pos(Succ(xy1000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy9000))) → False
new_flip(xy9, xy10, ba) → new_deleteBy1(xy10, xy9, ba)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Succ(xy1000)), Pos(Succ(xy9000))) → new_primEqNat0(xy1000, xy9000)
new_esEs(xy10, xy90, ty_Float) → error([])
new_esEs(xy10, xy90, app(ty_Maybe, cc)) → error([])
new_primEqInt(Neg(Zero), Neg(Zero)) → True

The set Q consists of the following terms:

new_esEs(x0, x1, ty_Integer)
new_esEs(x0, x1, ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs(x0, x1, ty_Ordering)
new_esEs(x0, x1, ty_Int)
new_primEqNat0(Zero, Succ(x0))
new_deleteBy1(x0, :(x1, x2), x3)
new_deleteBy00(x0, x1, x2, False, x3)
new_esEs(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_deleteBy1(x0, [], x1)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs(x0, x1, app(ty_Ratio, x2))
new_esEs(x0, x1, ty_Double)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqNat0(Zero, Zero)
new_primEqNat0(Succ(x0), Zero)
new_esEs(x0, x1, ty_Bool)
new_flip(x0, x1, x2)
new_esEs(x0, x1, app(ty_[], x2))
new_esEs(x0, x1, app(app(ty_@2, x2), x3))
new_esEs(x0, x1, ty_Char)
new_esEs(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_primEqNat0(Succ(x0), Succ(x1))
new_deleteBy00(x0, x1, x2, True, x3)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldl(xy9, xy10, :(xy110, xy111), ba) → new_foldl(new_flip(xy9, xy10, ba), xy110, xy111, ba)
The graph contains the following edges 3 > 2, 3 > 3, 4 >= 4

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_psPs(:(xy80, xy81), xy9, xy10, xy11, ba) → new_psPs(xy81, xy9, xy10, xy11, ba)

From the DPs we obtained the following set of size-change graphs:

new_psPs(:(xy80, xy81), xy9, xy10, xy11, ba) → new_psPs(xy81, xy9, xy10, xy11, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5

deleteBy0	ys y eq x True	= ys
deleteBy0	ys y eq x False	= y : deleteBy eq x ys

nubBy'	[] vy	= nubBy'3 [] vy
nubBy'	(y : ys) xs	= nubBy'2 (y : ys) xs

nubBy'1	y ys xs True	= nubBy' ys xs
nubBy'1	y ys xs False	= nubBy'0 y ys xs otherwise

nubByNubBy'1	xx y ys xs True	= nubByNubBy' xx ys xs
nubByNubBy'1	xx y ys xs False	= nubByNubBy'0 xx y ys xs otherwise

nubByNubBy'3	xx [] vy	= []
nubByNubBy'3	xx xv xw	= nubByNubBy'2 xx xv xw

nubByNubBy'	xx [] vy	= nubByNubBy'3 xx [] vy
nubByNubBy'	xx (y : ys) xs	= nubByNubBy'2 xx (y : ys) xs